\begin{tabbing}
links2Fifo{-}impl(${\it es}$;$l_{1}$;$l_{2}$;$A$;${\it tg}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<$$A$\+
\\[0ex], $A$
\\[0ex], \{$i$:Id$\mid$ ($i$ = source($l_{1}$) $\in$ Id) $\vee$ ($i$ = destination($l_{1}$) $\in$ Id)\} 
\\[0ex], $\lambda$$i$,$j$,$e$. es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id
\\[0ex]\& existse{-}at(\=${\it es}$;\+
\\[0ex]$j$;
\\[0ex]${\it e'}$.((\=(es{-}kind(${\it es}$; ${\it e'}$) = rcv($l_{1}$,${\it tg}$) $\in$ Knd)\+
\\[0ex]$\vee$ (es{-}kind(${\it es}$; ${\it e'}$) = rcv($l_{2}$,${\it tg}$) $\in$ Knd))
\-\\[0ex]\& es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$)))
\-\\[0ex], $\lambda$$i$,$e$. es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id
\\[0ex]\& ((es{-}kind(${\it es}$; $e$) = rcv($l_{1}$,${\it tg}$) $\in$ Knd) $\vee$ (es{-}kind(${\it es}$; $e$) = rcv($l_{2}$,${\it tg}$) $\in$ Knd))
\\[0ex], $\lambda$$i$,$x$,$y$. $x$ = $y$ $\in$ $A$
\\[0ex], $\cdot>$
\-
\end{tabbing}